1. The Field of the Invention
The invention relates to a method for verification of digital arithmetic circuits by means of an equivalence comparison between a specification circuit and an implementation circuit. Furthermore, the invention relates to an apparatus for carrying out this method.
2. The Relevant Technology
Procedures are known in which a so-called equivalence comparison is carried out (equivalence checking). On the one hand, this may be done by simulating all the possible combinations of input signals with the corresponding circuits. This exhaustive simulation has the disadvantage that, as the complexity of the circuits increases, the number of necessary computation operations rises correspondingly steeply. Although the use of graphical representations of Boolean functions according to R. Bryant, “Graph-based algorithms for Boolean function manipulation” (IEEE Transactions on Computers, C-35(8), 1986, and their further developments, allow considerably larger circuits to be handled than in the exhaustive simulation, even this procedure reaches its limits with most circuits of industrial size.
Attempts have thus likewise been made to investigate the circuits first of all on the basis of their structure. In this case, in two circuits which are to be compared,internal points which are equivalent are sought. This means that the logical signals which are present at these points in response to identical input signals are the same. In this way, it is possible to compare subregions of the circuits with one another. If it can be verified that these subregions are equivalent, this knowledge can be used directly in the subsequent investigation of further areas, thus allowing step-by-step equivalence comparison of the entire circuit. The input and output points of these internal subregions are in this case referred to as internal equivalence points (internal equivalences) or cut points. As an example of such methods, which are also referred to as “structural equivalence comparison”, reference should be made to D. Brand, “Verification of Large Synthesized Designs” in Proc. Intl. Conf. on Computer-Aided Design (ICCAD-93), pp. 543–547, 1993 and to W. Kunz, “An Efficient Tool for Logic Verification Based on Recursive Learning”, in Proc. Intl. Conference on Computer-Aided Design (ICCAD-93), 538–543, November 1993 and, in addition, to A. Kühlmann and F. Krohm, “Equivalence Checking Using Cuts and Heaps”, in Proc. Design Automation Conference (DAC-97), pp. 263–268, November 1997.
Methods for carrying out equivalence comparisons are used during circuit design. In this case, based on a first design (specification) which represents a desired circuit behaviour, this design is made specific by means of computer-assisted aids and by manual intervention by the designer in the corresponding circuit. In order to avoid faults from being introduced during this process, checks should be carried out during the synthesis of the circuit to determine whether the implementation at that time has the same behaviour as the specification at the higher level. It is therefore necessary during the equivalence comparison to determine the internal equivalence points or cut points between the design at the higher level and the circuit at that time.
This procedure has been found to be problematic in the case of circuit parts which relate to multiplication. The implementation is produced (after application of the relevant synthesis tools and possible manual actions) at gate level. In order now to allow the specification, which is at the register transfer level, to be compared with the implementation, it must be converted by the equivalence checker to a description at the gate level. In this case, it has been found to be problematic that the circuit derived from the design at the register transfer level has very major differences at the gate level in comparison with the design at gate level derived by means of the synthesis tools. This is essentially because different multiplication architectures are usual and there are a large number of implementation options for each individual architecture, so that in practice there are no equivalence points between the two circuits to be compared.
Methods which are based on decision diagrams at word level are known for equivalence comparison of arithmetic circuits. In this context, reference should be made, for example, to Bryant (TCAD85), Chen (ASP-DAC01). Since, however, the implementation is generally produced as a gate level description and there is too little information from the word level, the generation of these decision diagrams at word level is in practice often extremely complex in terms of computation and memory space.
Multipliers may be represented as a combination of two function blocks. In the first function block, the partial products of the multiplicand and the (binary) digits of the multiplier are formed. The partial products are designed to be dependent on whether the numbers to be multiplied may or may not have a negative mathematical sign, and also to be dependent on whether Booth recoding is used.